\begin{tabbing}
$\forall$${\it es}$:ES, $i$:Id, $L$:(IdLnk List), $T$:(Id$\rightarrow$Type).
\\[0ex]es{-}secret{-}server\=\{table:ut2, encrypt:ut2, decrypt:ut2\}\+
\\[0ex](${\it es}$; $T$; $L$; $i$)
\-\\[0ex]$\Rightarrow$ ($\forall$$e$:E. (loc($e$) = $i$) $\Rightarrow$ ($\parallel$"table" when $e$$\parallel$  = $\parallel$"table" when es{-}init(${\it es}$;$e$)$\parallel$  $\in$ $\mathbb{Z}$))
\end{tabbing}